Extend Solver Independent SMTLib2 Parser/Generator #436
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
… mantissa numbers than single or double precision
… mantissa numbers than single or double precision -allowed multiple operands for str.++ and re.++ in Parser and Generator
|
A problem within JavaSMT is that it allows only one single assert in an smt2 String. This needs to be corrected to support all Strings. Momentarily the Generator can be used as a workaround as it builds Strings with only one assert statement. |
…E CHANGED SOON! -added new test
DavidGalllob
force-pushed
the
extend-solver-independent-smtlib2-parser-generator
branch
from
95f9851 to
6b18557
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR extends JavaSMT with an independent SMTLib2 parser/generator layer.
Every solver can use the layer to generate or parse SMTLib2, independent of their own implementation.
The parsing directly uses the API of the solver.
Generating tracks all API usage independently into SMTLib2.
Additionally, we offer a complete solver-independent layer, that is usable with no solver installed. This layer can generate SMTLib2, but also parse SMTLib2 to manipulate the given formula.
Ideally, we also want to support usage of the solvers binaries with SMTLib2 directly. This has been tested for Princess, but has not been implemented for all solvers. My suggestion would be to remove/extract it from this PR and work on it separately.
TODO: